perm filename TEST2[F81,JMC]1 blob
sn#632513 filedate 1981-12-23 generic text, type C, neo UTF8
COMMENT ā VALID 00003 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 DCL(ISVAR (X))
C00003 00003 PROVE((IMPLIES (NOT (EQUAL (MATCH P E A) 'NO))
C00039 ENDMK
Cā;
DCL(ISVAR (X))
DEFN(ASSOC (P A)
(IF (LISTP A) (IF (EQUAL P (CAAR A)) (CAR A) (ASSOC P (CDR A))) NIL))
DEFN(SUBLIS (P A)
(IF (LISTP P)
(CONS (SUBLIS (CAR P) A) (SUBLIS (CDR P) A))
(IF (ISVAR P) (CDR (ASSOC P A)) P)))
DEFN (MATCH (P E A)
(IF (EQUAL A 'NO)
'NO
(IF (LISTP P)
(IF (LISTP E)
(MATCH (CAR P) (CAR E) (MATCH (CDR P) (CDR E) A))
'NO)
(IF (ISVAR P)
(IF (LISTP (ASSOC P A))
(IF (EQUAL E (CDR (ASSOC P A)))
A
'NO)
(CONS (CONS P E) A))
(IF (EQUAL P E) A 'NO)))))
PROVE((IMPLIES (NOT (EQUAL (MATCH P E A) 'NO))
(EQUAL (SUBLIS P (MATCH P E A)) E)))
This conjecture can be simplified, using the abbreviations NOT and
IMPLIES, to:
(IMPLIES (NOT (EQUAL (MATCH P E A) (QUOTE NO)))
(EQUAL (SUBLIS P (MATCH P E A)) E)).
Name the above subgoal *1.
We will try to prove it by induction. Five inductions are
suggested by terms in the conjecture. However, they merge into one
likely candidate induction. We will induct according to the following
scheme:
(AND (IMPLIES (NOT (LISTP P)) (p P E A))
(IMPLIES (AND (LISTP P)
(p (CAR P)
(CAR E)
(MATCH (CDR P) (CDR E) A))
(p (CDR P) (CDR E) A))
(p P E A))).
The inequalities CAR.LESSP and CDR.LESSP establish that the measure
(COUNT P) decreases according to the well-founded function LESSP in the
induction step of the scheme. Note, however, the inductive instances
chosen for E and A. The above induction scheme produces the following
five new conjectures:
Case 5. (IMPLIES (AND (NOT (LISTP P))
(NOT (EQUAL (MATCH P E A) (QUOTE NO))))
(EQUAL (SUBLIS P (MATCH P E A)) E)),
which we simplify, applying CDR.CONS and CAR.CONS, and expanding the
definitions of MATCH, ASSOC, SUBLIS, CDR, and LISTP, to five new
conjectures:
Case 5.5.
(IMPLIES (AND (NOT (LISTP P))
(NOT (EQUAL A (QUOTE NO)))
(ISVAR P)
(EQUAL E (CDR (ASSOC P A)))
(NOT (LISTP (ASSOC P A))))
(EQUAL (CDR (ASSOC P (CONS (CONS P E) A)))
E)),
which we again simplify, rewriting with the lemmas CDR.NLISTP,
CAR.CONS, and CDR.CONS, and expanding ASSOC and EQUAL, to:
T.
Case 5.4.
(IMPLIES (AND (NOT (LISTP P))
(EQUAL A (QUOTE NO))
(NOT (EQUAL (QUOTE NO) (QUOTE NO)))
(NOT (ISVAR P)))
(EQUAL P E)),
which we again simplify, unfolding EQUAL, to:
T.
Case 5.3.
(IMPLIES (AND (NOT (LISTP P))
(EQUAL A (QUOTE NO))
(NOT (EQUAL (QUOTE NO) (QUOTE NO)))
(ISVAR P))
(EQUAL 0 E)),
which we again simplify, unfolding the definition of EQUAL, to:
T.
Case 5.2.
(IMPLIES (AND (NOT (LISTP P))
(NOT (ISVAR P))
(NOT (EQUAL P E)))
(EQUAL (QUOTE NO) (QUOTE NO))).
This simplifies again, unfolding the function EQUAL, to:
T.
Case 5.1.
(IMPLIES (AND (NOT (LISTP P))
(ISVAR P)
(LISTP (ASSOC P A))
(NOT (EQUAL E (CDR (ASSOC P A))))
(NOT (EQUAL (QUOTE NO) (QUOTE NO))))
(EQUAL 0 E)).
However this simplifies again, unfolding the function EQUAL, to:
T.
Case 4. (IMPLIES (AND (LISTP P)
(EQUAL (MATCH (CAR P)
(CAR E)
(MATCH (CDR P) (CDR E) A))
(QUOTE NO))
(EQUAL (MATCH (CDR P) (CDR E) A)
(QUOTE NO))
(NOT (EQUAL (MATCH P E A) (QUOTE NO))))
(EQUAL (SUBLIS P (MATCH P E A)) E)),
which we simplify, expanding the definitions of EQUAL, MATCH, and
SUBLIS, to three new formulas:
collecting lists
9603, 10115 free cells
Case 4.3.
(IMPLIES
(AND (LISTP P)
(EQUAL (MATCH (CDR P) (CDR E) A)
(QUOTE NO))
(NOT (EQUAL A (QUOTE NO)))
(LISTP E)
(NOT (EQUAL (MATCH (CAR P)
(CAR E)
(MATCH (CDR P) (CDR E) A))
(QUOTE NO))))
(EQUAL (CONS (SUBLIS (CAR P)
(MATCH (CAR P)
(CAR E)
(MATCH (CDR P) (CDR E) A)))
(SUBLIS (CDR P)
(MATCH (CAR P)
(CAR E)
(MATCH (CDR P) (CDR E) A))))
E)).
This again simplifies, expanding EQUAL and MATCH, to:
T.
Case 4.2.
(IMPLIES (AND (LISTP P)
(EQUAL (MATCH (CDR P) (CDR E) A)
(QUOTE NO))
(EQUAL A (QUOTE NO))
(NOT (EQUAL (QUOTE NO) (QUOTE NO))))
(EQUAL (CONS (SUBLIS (CAR P) (QUOTE NO))
(SUBLIS (CDR P) (QUOTE NO)))
E)).
But this simplifies again, expanding the functions EQUAL and MATCH,
to:
T.
Case 4.1.
(IMPLIES (AND (LISTP P)
(EQUAL (MATCH (CDR P) (CDR E) A)
(QUOTE NO))
(NOT (LISTP E)))
(EQUAL (QUOTE NO) (QUOTE NO))).
This simplifies again, rewriting with CDR.NLISTP, and expanding the
definitions of LISTP and MATCH, to:
T.
Case 3. (IMPLIES (AND (LISTP P)
(EQUAL (SUBLIS (CAR P)
(MATCH (CAR P)
(CAR E)
(MATCH (CDR P) (CDR E) A)))
(CAR E))
(EQUAL (MATCH (CDR P) (CDR E) A)
(QUOTE NO))
(NOT (EQUAL (MATCH P E A) (QUOTE NO))))
(EQUAL (SUBLIS P (MATCH P E A)) E)),
which simplifies, opening up the definitions of EQUAL, MATCH, and
SUBLIS, to three new conjectures:
Case 3.3.
(IMPLIES
(AND (LISTP P)
(EQUAL (SUBLIS (CAR P) (QUOTE NO))
(CAR E))
(EQUAL (MATCH (CDR P) (CDR E) A)
(QUOTE NO))
(NOT (EQUAL A (QUOTE NO)))
(LISTP E)
(NOT (EQUAL (MATCH (CAR P)
(CAR E)
(MATCH (CDR P) (CDR E) A))
(QUOTE NO))))
(EQUAL (CONS (SUBLIS (CAR P)
(MATCH (CAR P)
(CAR E)
(MATCH (CDR P) (CDR E) A)))
(SUBLIS (CDR P)
(MATCH (CAR P)
(CAR E)
(MATCH (CDR P) (CDR E) A))))
E)).
This again simplifies, expanding the definitions of EQUAL and MATCH,
to:
T.
Case 3.2.
(IMPLIES (AND (LISTP P)
(EQUAL (SUBLIS (CAR P) (QUOTE NO))
(CAR E))
(EQUAL (MATCH (CDR P) (CDR E) A)
(QUOTE NO))
(EQUAL A (QUOTE NO))
(NOT (EQUAL (QUOTE NO) (QUOTE NO))))
(EQUAL (CONS (SUBLIS (CAR P) (QUOTE NO))
(SUBLIS (CDR P) (QUOTE NO)))
E)),
which again simplifies, expanding the functions EQUAL and MATCH, to:
T.
Case 3.1.
(IMPLIES (AND (LISTP P)
(EQUAL (SUBLIS (CAR P) (QUOTE NO))
(CAR E))
(EQUAL (MATCH (CDR P) (CDR E) A)
(QUOTE NO))
(NOT (LISTP E)))
(EQUAL (QUOTE NO) (QUOTE NO))).
However this simplifies again, applying CAR.NLISTP and CDR.NLISTP,
and expanding the definitions of LISTP and MATCH, to:
T.
Case 2. (IMPLIES (AND (LISTP P)
(EQUAL (MATCH (CAR P)
(CAR E)
(MATCH (CDR P) (CDR E) A))
(QUOTE NO))
(EQUAL (SUBLIS (CDR P)
(MATCH (CDR P) (CDR E) A))
(CDR E))
(NOT (EQUAL (MATCH P E A) (QUOTE NO))))
(EQUAL (SUBLIS P (MATCH P E A)) E)).
This simplifies, opening up the definitions of MATCH and SUBLIS, to
the following two new goals:
collecting lists
9913, 10425 free cells
Case 2.2.
(IMPLIES (AND (LISTP P)
(EQUAL (MATCH (CAR P)
(CAR E)
(MATCH (CDR P) (CDR E) A))
(QUOTE NO))
(EQUAL (SUBLIS (CDR P)
(MATCH (CDR P) (CDR E) A))
(CDR E))
(NOT (LISTP E)))
(EQUAL (QUOTE NO) (QUOTE NO))).
This simplifies again, rewriting with CAR.NLISTP and CDR.NLISTP,
and opening up the definitions of LISTP and MATCH, to:
T.
Case 2.1.
(IMPLIES (AND (LISTP P)
(EQUAL (MATCH (CAR P)
(CAR E)
(MATCH (CDR P) (CDR E) A))
(QUOTE NO))
(EQUAL (SUBLIS (CDR P)
(MATCH (CDR P) (CDR E) A))
(CDR E))
(EQUAL A (QUOTE NO))
(NOT (EQUAL (QUOTE NO) (QUOTE NO))))
(EQUAL (CONS (SUBLIS (CAR P) (QUOTE NO))
(SUBLIS (CDR P) (QUOTE NO)))
E)).
This simplifies again, expanding EQUAL and MATCH, to:
T.
Case 1. (IMPLIES (AND (LISTP P)
(EQUAL (SUBLIS (CAR P)
(MATCH (CAR P)
(CAR E)
(MATCH (CDR P) (CDR E) A)))
(CAR E))
(EQUAL (SUBLIS (CDR P)
(MATCH (CDR P) (CDR E) A))
(CDR E))
(NOT (EQUAL (MATCH P E A) (QUOTE NO))))
(EQUAL (SUBLIS P (MATCH P E A)) E)),
which simplifies, expanding MATCH and SUBLIS, to three new
conjectures:
collecting lists
10411, 10411 free cells
Case 1.3.
(IMPLIES
(AND (LISTP P)
(EQUAL (SUBLIS (CAR P)
(MATCH (CAR P)
(CAR E)
(MATCH (CDR P) (CDR E) A)))
(CAR E))
(EQUAL (SUBLIS (CDR P)
(MATCH (CDR P) (CDR E) A))
(CDR E))
(NOT (EQUAL A (QUOTE NO)))
(LISTP E)
(NOT (EQUAL (MATCH (CAR P)
(CAR E)
(MATCH (CDR P) (CDR E) A))
(QUOTE NO))))
(EQUAL (CONS (SUBLIS (CAR P)
(MATCH (CAR P)
(CAR E)
(MATCH (CDR P) (CDR E) A)))
(SUBLIS (CDR P)
(MATCH (CAR P)
(CAR E)
(MATCH (CDR P) (CDR E) A))))
E)).
Applying the lemma CAR/CDR.ELIM, replace P by (CONS X Z) to
eliminate (CAR P) and (CDR P). We would thus like to prove the new
conjecture:
(IMPLIES
(AND (EQUAL (SUBLIS X
(MATCH X (CAR E) (MATCH Z (CDR E) A)))
(CAR E))
(EQUAL (SUBLIS Z (MATCH Z (CDR E) A))
(CDR E))
(NOT (EQUAL A (QUOTE NO)))
(LISTP E)
(NOT (EQUAL (MATCH X (CAR E) (MATCH Z (CDR E) A))
(QUOTE NO))))
(EQUAL (CONS (SUBLIS X
(MATCH X (CAR E) (MATCH Z (CDR E) A)))
(SUBLIS Z
(MATCH X
(CAR E)
(MATCH Z (CDR E) A))))
E)).
Appealing to the lemma CAR/CDR.ELIM, we now replace E by (CONS V W)
to eliminate (CAR E) and (CDR E). We thus obtain:
(IMPLIES (AND (EQUAL (SUBLIS X (MATCH X V (MATCH Z W A)))
V)
(EQUAL (SUBLIS Z (MATCH Z W A)) W)
(NOT (EQUAL A (QUOTE NO)))
(NOT (EQUAL (MATCH X V (MATCH Z W A))
(QUOTE NO))))
(EQUAL (CONS (SUBLIS X (MATCH X V (MATCH Z W A)))
(SUBLIS Z (MATCH X V (MATCH Z W A))))
(CONS V W))).
This further simplifies, applying CONS.EQUAL, to:
(IMPLIES (AND (EQUAL (SUBLIS X (MATCH X V (MATCH Z W A)))
V)
(EQUAL (SUBLIS Z (MATCH Z W A)) W)
(NOT (EQUAL A (QUOTE NO)))
(NOT (EQUAL (MATCH X V (MATCH Z W A))
(QUOTE NO))))
(EQUAL (SUBLIS Z (MATCH X V (MATCH Z W A)))
W)).
We use the first equality hypothesis by substituting:
(SUBLIS X (MATCH X V (MATCH Z W A)))
for V and throwing away the equality. This generates:
(IMPLIES
(AND (EQUAL (SUBLIS Z (MATCH Z W A)) W)
(NOT (EQUAL A (QUOTE NO)))
(NOT (EQUAL (MATCH X
(SUBLIS X (MATCH X V (MATCH Z W A)))
(MATCH Z W A))
(QUOTE NO))))
(EQUAL (SUBLIS Z
(MATCH X
(SUBLIS X (MATCH X V (MATCH Z W A)))
(MATCH Z W A)))
W)).
We use the above equality hypothesis by cross-fertilizing
(SUBLIS Z (MATCH Z W A)) for W and throwing away the equality.
This produces:
(IMPLIES
(AND (NOT (EQUAL A (QUOTE NO)))
(NOT (EQUAL (MATCH X
(SUBLIS X (MATCH X V (MATCH Z W A)))
(MATCH Z W A))
(QUOTE NO))))
(EQUAL (SUBLIS Z
(MATCH X
(SUBLIS X (MATCH X V (MATCH Z W A)))
(MATCH Z W A)))
(SUBLIS Z (MATCH Z W A)))),
which we generalize by replacing (MATCH Z W A) by Y. This
generates:
(IMPLIES (AND (NOT (EQUAL A (QUOTE NO)))
(NOT (EQUAL (MATCH X (SUBLIS X (MATCH X V Y)) Y)
(QUOTE NO))))
(EQUAL (SUBLIS Z
(MATCH X (SUBLIS X (MATCH X V Y)) Y))
(SUBLIS Z Y))),
which we generalize by replacing (MATCH X V Y) by U. This
generates:
(IMPLIES (AND (NOT (EQUAL A (QUOTE NO)))
(NOT (EQUAL (MATCH X (SUBLIS X U) Y)
(QUOTE NO))))
(EQUAL (SUBLIS Z (MATCH X (SUBLIS X U) Y))
(SUBLIS Z Y))),
which we generalize by replacing (SUBLIS X U) by B. We thus obtain:
(IMPLIES (AND (NOT (EQUAL A (QUOTE NO)))
(NOT (EQUAL (MATCH X B Y) (QUOTE NO))))
(EQUAL (SUBLIS Z (MATCH X B Y))
(SUBLIS Z Y))).
We will try to prove the above conjecture by generalizing it,
replacing (MATCH X B Y) by U. The result is:
collecting lists
10095, 10095 free cells
(IMPLIES (AND (NOT (EQUAL A (QUOTE NO)))
(NOT (EQUAL U (QUOTE NO))))
(EQUAL (SUBLIS Z U) (SUBLIS Z Y))).
Eliminate the irrelevant term. This produces:
(IMPLIES (NOT (EQUAL U (QUOTE NO)))
(EQUAL (SUBLIS Z U) (SUBLIS Z Y))),
which we will finally name *1.1.
Case 1.2.
(IMPLIES
(AND (LISTP P)
(EQUAL (SUBLIS (CAR P)
(MATCH (CAR P)
(CAR E)
(MATCH (CDR P) (CDR E) A)))
(CAR E))
(EQUAL (SUBLIS (CDR P)
(MATCH (CDR P) (CDR E) A))
(CDR E))
(EQUAL A (QUOTE NO))
(NOT (EQUAL (QUOTE NO) (QUOTE NO))))
(EQUAL (CONS (SUBLIS (CAR P) (QUOTE NO))
(SUBLIS (CDR P) (QUOTE NO)))
E)),
which we again simplify, unfolding the definitions of EQUAL and
MATCH, to:
T.
collecting lists
9295, 10319 free cells
collecting lists
10289, 10289 free cells
Case 1.1.
(IMPLIES
(AND (LISTP P)
(EQUAL (SUBLIS (CAR P)
(MATCH (CAR P)
(CAR E)
(MATCH (CDR P) (CDR E) A)))
(CAR E))
(EQUAL (SUBLIS (CDR P)
(MATCH (CDR P) (CDR E) A))
(CDR E))
(NOT (LISTP E)))
(EQUAL (QUOTE NO) (QUOTE NO))).
However this simplifies again, applying CAR.NLISTP, CDR.NLISTP,
CDR.CONS, and CAR.CONS, and unfolding LISTP, MATCH, EQUAL, ASSOC,
and SUBLIS, to:
T.
So let us turn our attention to:
(IMPLIES (NOT (EQUAL U (QUOTE NO)))
(EQUAL (SUBLIS Z U) (SUBLIS Z Y))),
which is formula *1.1 above. Perhaps we can prove it by induction.
There are two plausible inductions. However, they merge into one
likely candidate induction. We will induct according to the following
scheme:
(AND (IMPLIES (NOT (LISTP Z)) (p Z U Y))
(IMPLIES (AND (LISTP Z)
(p (CDR Z) U Y)
(p (CAR Z) U Y))
(p Z U Y))).
The inequalities CAR.LESSP and CDR.LESSP establish that the measure
(COUNT Z) decreases according to the well-founded function LESSP in the
induction step of the scheme. The above induction scheme generates two
new formulas:
Case 2. (IMPLIES (AND (NOT (LISTP Z))
(NOT (EQUAL U (QUOTE NO))))
(EQUAL (SUBLIS Z U) (SUBLIS Z Y))),
which simplifies, expanding the definition of SUBLIS, to two new
formulas:
Case 2.2.
(IMPLIES (AND (NOT (LISTP Z))
(NOT (EQUAL U (QUOTE NO)))
(NOT (ISVAR Z)))
(EQUAL Z Z)),
which again simplifies, obviously, to:
T.
collecting lists
11687, 11687 free cells
Case 2.1.
(IMPLIES (AND (NOT (LISTP Z))
(NOT (EQUAL U (QUOTE NO)))
(ISVAR Z))
(EQUAL (CDR (ASSOC Z U))
(CDR (ASSOC Z Y)))).
Give the above formula the name *1.1.1.
Case 1. (IMPLIES (AND (LISTP Z)
(EQUAL (SUBLIS (CDR Z) U)
(SUBLIS (CDR Z) Y))
(EQUAL (SUBLIS (CAR Z) U)
(SUBLIS (CAR Z) Y))
(NOT (EQUAL U (QUOTE NO))))
(EQUAL (SUBLIS Z U) (SUBLIS Z Y))),
which we simplify, rewriting with CONS.EQUAL, and expanding the
definition of SUBLIS, to:
T.
So let us turn our attention to:
(IMPLIES (AND (NOT (LISTP Z))
(NOT (EQUAL U (QUOTE NO)))
(ISVAR Z))
(EQUAL (CDR (ASSOC Z U))
(CDR (ASSOC Z Y)))),
which we named *1.1.1 above. We will try to prove it by induction.
Two inductions are suggested by terms in the conjecture, both of which
are unflawed. Since both of these are equally likely, we will choose
arbitrarily. We will induct according to the following scheme:
(AND (IMPLIES (NOT (LISTP U)) (p Z U Y))
(IMPLIES (EQUAL Z (CAAR U)) (p Z U Y))
(IMPLIES (AND (LISTP U)
(NOT (EQUAL Z (CAAR U)))
(p Z (CDR U) Y))
(p Z U Y))).
The inequality CDR.LESSP establishes that the measure (COUNT U)
decreases according to the well-founded function LESSP in the induction
step of the scheme. The above induction scheme produces the following
four new formulas:
Case 4. (IMPLIES (AND (NOT (LISTP U))
(NOT (LISTP Z))
(NOT (EQUAL U (QUOTE NO)))
(ISVAR Z))
(EQUAL (CDR (ASSOC Z U))
(CDR (ASSOC Z Y)))),
which we simplify, opening up the definitions of ASSOC and CDR, to:
(IMPLIES (AND (NOT (LISTP U))
(NOT (LISTP Z))
(NOT (EQUAL U (QUOTE NO)))
(ISVAR Z))
(EQUAL 0 (CDR (ASSOC Z Y)))),
which has two irrelevant terms in it. By eliminating these terms we
get the new conjecture:
(IMPLIES (AND (NOT (LISTP Z)) (ISVAR Z))
(EQUAL 0 (CDR (ASSOC Z Y)))),
which we will name *1.1.1.1.
Case 3. (IMPLIES (AND (EQUAL Z (CAAR U))
(NOT (LISTP Z))
(NOT (EQUAL U (QUOTE NO)))
(ISVAR Z))
(EQUAL (CDR (ASSOC Z U))
(CDR (ASSOC Z Y)))).
This simplifies, expanding the definition of ASSOC, to two new
conjectures:
Case 3.2.
(IMPLIES (AND (NOT (LISTP (CAAR U)))
(NOT (EQUAL U (QUOTE NO)))
(ISVAR (CAAR U))
(NOT (LISTP U)))
(EQUAL (CDR NIL)
(CDR (ASSOC (CAAR U) Y)))).
This again simplifies, applying the lemma CAR.NLISTP, and expanding
the functions CAR, LISTP, and CDR, to:
(IMPLIES (AND (NOT (EQUAL U (QUOTE NO)))
(ISVAR 0)
(NOT (LISTP U)))
(EQUAL 0 (CDR (ASSOC 0 Y)))),
which has three irrelevant terms in it. By eliminating these terms
we get:
(EQUAL 0 (CDR (ASSOC 0 Y))),
which we will name *1.1.1.2.
Case 3.1.
(IMPLIES (AND (NOT (LISTP (CAAR U)))
(NOT (EQUAL U (QUOTE NO)))
(ISVAR (CAAR U))
(LISTP U))
(EQUAL (CDAR U)
(CDR (ASSOC (CAAR U) Y)))),
which again simplifies, clearly, to:
(IMPLIES (AND (NOT (LISTP (CAAR U)))
(ISVAR (CAAR U))
(LISTP U))
(EQUAL (CDAR U)
(CDR (ASSOC (CAAR U) Y)))).
Appealing to the lemma CAR/CDR.ELIM, we now replace U by (CONS X V)
to eliminate (CAR U) and (CDR U) and X by (CONS W D) to eliminate
(CAR X) and (CDR X). This produces two new formulas:
Case 3.1.2.
(IMPLIES (AND (NOT (LISTP X))
(NOT (LISTP (CAR X)))
(ISVAR (CAR X)))
(EQUAL (CDR X)
(CDR (ASSOC (CAR X) Y)))).
This simplifies further, applying CAR.NLISTP and CDR.NLISTP, and
expanding the function LISTP, to:
(IMPLIES (AND (NOT (LISTP X)) (ISVAR 0))
(EQUAL 0 (CDR (ASSOC 0 Y)))).
Eliminate irrelevant terms. We thus obtain the conjecture:
(EQUAL 0 (CDR (ASSOC 0 Y))).
Name the above subgoal *1.1.1.3.
Case 3.1.1.
(IMPLIES (AND (NOT (LISTP W)) (ISVAR W))
(EQUAL D (CDR (ASSOC W Y)))).
Give the above formula the name *1.1.1.4.
Case 2. (IMPLIES (AND (LISTP U)
(NOT (EQUAL Z (CAAR U)))
(EQUAL (CDR U) (QUOTE NO))
(NOT (LISTP Z))
(NOT (EQUAL U (QUOTE NO)))
(ISVAR Z))
(EQUAL (CDR (ASSOC Z U))
(CDR (ASSOC Z Y)))).
This simplifies, expanding the definition of ASSOC, to:
(IMPLIES (AND (LISTP U)
(NOT (EQUAL Z (CAAR U)))
(EQUAL (CDR U) (QUOTE NO))
(NOT (LISTP Z))
(ISVAR Z))
(EQUAL (CDR (ASSOC Z (CDR U)))
(CDR (ASSOC Z Y)))).
But this simplifies again, expanding the definitions of LISTP, ASSOC,
and CDR, to:
(IMPLIES (AND (LISTP U)
(NOT (EQUAL Z (CAAR U)))
(EQUAL (CDR U) (QUOTE NO))
(NOT (LISTP Z))
(ISVAR Z))
(EQUAL 0 (CDR (ASSOC Z Y)))).
Applying the lemma CAR/CDR.ELIM, we now replace U by (CONS X V) to
eliminate (CAR U) and (CDR U) and X by (CONS W D) to eliminate
(CAR X) and (CDR X). The result is the following two new conjectures:
Case 2.2.
(IMPLIES (AND (NOT (LISTP X))
(NOT (EQUAL Z (CAR X)))
(EQUAL V (QUOTE NO))
(NOT (LISTP Z))
(ISVAR Z))
(EQUAL 0 (CDR (ASSOC Z Y)))).
This simplifies further, rewriting with CAR.NLISTP, to the
conjecture:
(IMPLIES (AND (NOT (LISTP X))
(NOT (EQUAL Z 0))
(NOT (LISTP Z))
(ISVAR Z))
(EQUAL 0 (CDR (ASSOC Z Y)))),
which has an irrelevant term in it. By eliminating the term we get:
(IMPLIES (AND (NOT (EQUAL Z 0))
(NOT (LISTP Z))
(ISVAR Z))
(EQUAL 0 (CDR (ASSOC Z Y)))),
which we will name *1.1.1.5.
Case 2.1.
(IMPLIES (AND (NOT (EQUAL Z W))
(EQUAL V (QUOTE NO))
(NOT (LISTP Z))
(ISVAR Z))
(EQUAL 0 (CDR (ASSOC Z Y)))).
Of course, this simplifies further, obviously, to:
(IMPLIES (AND (NOT (EQUAL Z W))
(NOT (LISTP Z))
(ISVAR Z))
(EQUAL 0 (CDR (ASSOC Z Y)))),
which we will name *1.1.1.6.
collecting lists
11248, 11248 free cells
Case 1. (IMPLIES (AND (LISTP U)
(NOT (EQUAL Z (CAAR U)))
(EQUAL (CDR (ASSOC Z (CDR U)))
(CDR (ASSOC Z Y)))
(NOT (LISTP Z))
(NOT (EQUAL U (QUOTE NO)))
(ISVAR Z))
(EQUAL (CDR (ASSOC Z U))
(CDR (ASSOC Z Y)))),
which we simplify, expanding ASSOC, to:
T.
So next consider:
(IMPLIES (AND (NOT (EQUAL Z W))
(NOT (LISTP Z))
(ISVAR Z))
(EQUAL 0 (CDR (ASSOC Z Y)))),
which we named *1.1.1.6 above. But this conjecture is subsumed by
formula *1.1.1.4 above.
So we now return to:
(IMPLIES (AND (NOT (EQUAL Z 0))
(NOT (LISTP Z))
(ISVAR Z))
(EQUAL 0 (CDR (ASSOC Z Y)))),
which we named *1.1.1.5 above. This conjecture is subsumed by the
subgoal we named *1.1.1.4 above.
So let us turn our attention to:
(IMPLIES (AND (NOT (LISTP W)) (ISVAR W))
(EQUAL D (CDR (ASSOC W Y)))),
which we named *1.1.1.4 above. Let us appeal to the induction
principle. There is only one suggested induction. We will induct
according to the following scheme:
(AND (IMPLIES (NOT (LISTP Y)) (p D W Y))
(IMPLIES (EQUAL W (CAAR Y)) (p D W Y))
(IMPLIES (AND (LISTP Y)
(NOT (EQUAL W (CAAR Y)))
(p D W (CDR Y)))
(p D W Y))).
The inequality CDR.LESSP establishes that the measure (COUNT Y)
decreases according to the well-founded function LESSP in the induction
step of the scheme. The above induction scheme produces three new
goals:
Case 3. (IMPLIES (AND (NOT (LISTP Y))
(NOT (LISTP W))
(ISVAR W))
(EQUAL D (CDR (ASSOC W Y)))),
which simplifies, expanding the definitions of ASSOC and CDR, to:
(IMPLIES (AND (NOT (LISTP Y))
(NOT (LISTP W))
(ISVAR W))
(EQUAL D 0)).
Eliminate irrelevant terms. This produces the new formula:
F,
which means the proof attempt has
************** F A I L E D **************